COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	ideas[s84,jmc]		circum vs. default logic
C00003 00003	apr 23 - automatic abbreviation macros in editors
C00004 00004	apr 28 - Termination of Ackermann by induction on higher type
C00005 00005	may 21 - partial models, etc.
C00007 00006	June 5 - Prize contest in programming
C00009 ENDMK
C⊗;
ideas[s84,jmc]		circum vs. default logic

default logic can infer consistency of arith, but disj. and circum
is more nearly effective

takasu

1. We infer that something is best, because it is consistent that it
the best.  Circumscribe  better(x,candidate).

2. The bolder conjectures are made by circumscribing w/r subsets
of the available facts.

apr 23 - automatic abbreviation macros in editors
What about a program that investigated what words and phrases a person used
frequently and then offered a set of macros that abbreviated them?
One cculd imagine putting E or some other editor in a collect mode
for the purpose of accumulating the statistics.

apr 28 - Termination of Ackermann by induction on higher type
Can we get termination of Ackermann function by a simple recursion
on a higher type?  What about the Goodstein function?  Perhaps it
requires recursion of some transfinite type.  What about higher
combinators?  Is there some generalization of  mapcar  which is
a combinator?

may 21 - partial models, etc.
Introduce Q as a parameter only parenthetically.

Parametrization of Boolean functions.  Investigate which Boolean
functions don't split into Boolean functions of functions of
disjoint subsets of the variables.  Partial splitting as in
incompletely reducible representations.  The counting functions,
e.g. 3 of p q r s t  provide examples indecomposability.

Partial models and their relation to JK's direct proof.  Proving
∃x∀y(Px ⊃ Py) involves disproving Px ∧ ¬Pfx.  This is not "obvious",
but disproving  Px ∧ ¬Pfx ∧ Pu ∧ ¬Pgu  is "obvious".

In propositional circumscription, we really can just minimize
Axiom ⊃ E  rather than minimize  E  holding Axiom.

June 5 - Prize contest in programming
	Suppose there were a large prize ≥$50K for a program to
be written in 3 months to do something interesting.  Besides the
prize, selected applicants would receive $3000 for the three months
work.  If there were 5 applicants selected for subsidy, this would
cost another $15K.  The idea is that while the prize would be
all-or-nothing to the best solution, qualified people could afford
to invest their time.  It might be allowable to form teams to compete,
but there would be only one subsidy per team.

Now we have only to figure out what the program should do.  Possibilities
include (1) chess program for IBM pc that says what it thinks and
enters the public domain.  (2) Display editor.  (3) Consumer expert
system.  Here the different groups can solve different problems.
Perhaps common lisp should be specified as the language.
Perhaps Inference could offer such contest for an ART based system,
but ART would have to be thoroughly debugged first.